$\forall$$T$:Type, $f$:($T$$\rightarrow$$T$).
\\[0ex]retraction($T$;$f$) $\Rightarrow$ ($\forall$$y$, $x$:$T$. $y$ is $f$$\ast$($x$) $\Rightarrow$ $f$($x$) is $f$$\ast$($y$) $\Rightarrow$ (($y$ = $x$) $\vee$ ($y$ = $f$($x$))))